#include "fraig.h"
#include <tr1/unordered_set>
#include <iostream>
using std::cout;
using std::endl;

static size_t seed = 0x19850225;
void mysrand( unsigned x ){ seed = x; }
static size_t myrand(){ return seed = (1103515245UL * seed + 123456789UL); }

///////////////////////////////////////////////////////////////////////////////
//                      PATTERN FUNCTION                                     //
///////////////////////////////////////////////////////////////////////////////
typedef Minisat::vec<Minisat::Lit> Clause;
struct Pattern
{ 
   uint64_t dat[PATSIZE]; 
   static int end;
   uint64_t last(){return dat[end-1];}
   uint64_t key();
   void rand( unsigned i );
   void sim00( uint64_t * a , uint64_t * b );
   void sim10( uint64_t * a , uint64_t * b );
   void sim01( uint64_t * a , uint64_t * b );
   void sim11( uint64_t * a , uint64_t * b );
};
int Pattern::end = 0;
void Pattern::rand( unsigned i ){
   for( ; i < (unsigned)end ; ++ i )
      dat[i] = myrand();
}
void Pattern::sim00( uint64_t * a , uint64_t * b ){
   for( int i = 0 ; i < end ; ++ i )dat[i] = a[i] & b[i];
}
void Pattern::sim10( uint64_t * a , uint64_t * b ){
   for( int i = 0 ; i < end ; ++ i )dat[i] = (~a[i]) & b[i];
}
void Pattern::sim01( uint64_t * a , uint64_t * b ){
   for( int i = 0 ; i < end ; ++ i )dat[i] = a[i] & (~b[i]);
}
void Pattern::sim11( uint64_t * a , uint64_t * b ){
   for( int i = 0 ; i < end ; ++ i )dat[i] = ~(a[i] | b[i]);
}
inline void folding_pattern( uint64_t * dat , unsigned end , uint8_t ph)
{
   dat[0] = dat[0] ^ -((uint64_t)(ph&end--));
   while( end )dat[0] ^= dat[ end -- ]; 
}
///////////////////////////////////////////////////////////////////////////////
//                      STATIC FUNCTION                                      //
///////////////////////////////////////////////////////////////////////////////
inline bool eq( const Pattern & a , const Pattern & b ){
   for( int i = 0 ; i < Pattern::end ; ++i )
      if( a.dat[i] != b.dat[i] ) return false;
   return true;
}
inline bool inv( const Pattern & a , const Pattern & b ){
   for( int i = 0 ; i < Pattern::end ; ++i )
      if( (a.dat[i] ^ b.dat[i]) +1 )  return false;
   return true;
}
inline bool dual_eq( const Pattern & a , const Pattern & b )
{ 
   return eq( a , b ) || inv( a , b ) ; 
}
///////////////////////////////////////////////////////////////////////////////
//                      FUNCTION OBJECT                                      //
///////////////////////////////////////////////////////////////////////////////
struct PatHash{
   const Pattern * pats;
   inline size_t operator()( unsigned i ) const{ return pats[i].dat[0] ; }
   PatHash( const Pattern * a ): pats(a){}
};
struct PatLt{
   const Pattern * pats;
   inline bool operator()( unsigned a , unsigned b) const
   { 
      if( pats[a].dat[0] != pats[b].dat[0] )
         return pats[a].dat[0] < pats[b].dat[0];
      return a < b ;
   }
   PatLt( const Pattern * a ): pats(a){}
};
struct PatEq
{
   unsigned * eqn;
   int * idx;
   const Pattern * pats;

   bool operator()( unsigned a , unsigned b )const
   {
      if( pats[a].dat[0] != pats[b].dat[0] ) return false;
      idx[b]+= 1; eqn[a]=b;
      return true;
   }
   PatEq( unsigned * e , int * i , const Pattern *p ):eqn(e),idx(i),pats(p){}
};
///////////////////////////////////////////////////////////////////////////////
//                      PARTITION STATIC FUNCTION                            //
///////////////////////////////////////////////////////////////////////////////
static void sub_partition_dual( const Pattern * p , unsigned * eqn ,int * & s  , int * & ns )
{
   if( dual_eq( p[ *s ] , p[*(s+1) ] ) )
   {
      *ns++=3;
      *ns++=*s++;
      *ns++=*s++;
   }else
   {
      int n = *s++; eqn[n]=n;
          n = *s++; eqn[n]=n;
   }
}
static void sub_partition_sort( const Pattern * p , unsigned * eqn , int * & s , int * e , int * & ns )
{
   std::sort( s , e , PatLt( p ));
   for( int * f = s +1 ; s != e ; ++ f )
   {
      if( f != e && p[ *f ].dat[0] == p[ *s ].dat[0] )continue;
      else if( f-s > 1 )
      {
         *ns++ = f-s + 1;
         int ref = *s;
         while( s != f )
         {
            int n = *s++;
            *ns++ = n;
            eqn[n] = ref;
         }
      }
      else
      {
         int n = *s++;
         eqn[n]=n;
      }
   }
}
static void sub_partition_hash( const Pattern * p , unsigned * eqn , int * idx , int * & s , int * e , int * & ns )
{
   typedef std::tr1::unordered_set<unsigned,PatHash,PatEq> hash_t;

   hash_t hash(e-s,PatHash( p ),PatEq( eqn , idx , p));
   for( int * i = s ; i != e  ; ++ i )
   {
      int n = *i;
      hash.insert( eqn[n]=n ); 
   }

   int * nns = ns;
   for( int * i = s ; i < e ; ++ i )
   {
      unsigned n = *i; assert( n != -1 );
      if( idx[n] )
      {
         unsigned gsz = idx[n];
         *ns = gsz + 2;
         idx[n] = ns-nns + 1 ;
         ns += gsz + 2 ;
         *(nns + idx[n] ++ ) = n ;
      }
      if( eqn[n] != n )
         *(nns+idx[eqn[n]]++)=n;
   }
   while( s != e ) idx[ *s++ ] = 0;
}
static void sub_partition_linear( const Pattern * p , unsigned * eqn , int * & s , int * e , int * & ns )
{
   if( s == e )return;

   int *c = ns++ ,  r = *ns++ = *s , * t = s;
   *c=2;

   for( int * i = s+1 ; i != e ; ++ i )
      if( p[*i].dat[0] == p[r].dat[0] )
      {
         eqn[ *ns++=*i ] = r ;
         (*c)++;
      }else
         *t++=*i;
   if( (*c) == 2 ) ns-=2;
  
   eqn[ *s ] = *s;
   sub_partition_linear( p , eqn , s , t , ns);
}
///////////////////////////////////////////////////////////////////////////////
//                      FRAIG MEMBER FUNCTION                                //
///////////////////////////////////////////////////////////////////////////////
void Fraig::init()
{
   CktCover::init( false );
   _pats = new Pattern [sz];
   _idx   = new int [sz]; 

   _eqn   = new unsigned [sz];
   _group = new int [sz+(sz>>1)+2];
   _ngroup= new int [sz+(sz>>1)+2];
   _deplvl= new int [sz];

   memset( _eqn , 0 , sizeof( unsigned ) * sz );
   memset( _idx , 0 , sizeof( int ) * sz );

   _group[0]    = sz+1;
   _group[sz+1] = 1;
   for( unsigned i = 0 ; i < sz ; ++ i ) _group[i+1] = i;
   memset( _pats[0].dat , 0 , sizeof( uint64_t ) * PATSIZE );

   _npat=0;
   _selptr=1;
   _end=_group[0];
}
Fraig::~Fraig()
{
   delete [] _eqn;
   delete [] _deplvl;

   delete [] _group;
   delete [] _idx; 
   delete [] _ngroup;

   delete [] _pats;
   if( _stages.size() ) 
      delete [] _stages[0].dat; 
}
///////////////////////////////////////////////////////////////////////////////
//                      FRAIG SIMULATION                                     //
///////////////////////////////////////////////////////////////////////////////

void Fraig::pat_init_rand( )
{
   for( unsigned i = 1 ; i < _andFlag ; ++i ) 
      _pats[i].rand(0);
}
void Fraig::simulation()
{
   for( unsigned i = _andFlag; i != sz ; ++ i )
   {
      const AigNode n = data[i];
      if( sign( n.fanin[0] ) )
      {
         if( sign( n.fanin[1] ) )
            _pats[i].sim11( _pats[ var(n.fanin[0]) ].dat , _pats[ var(n.fanin[1]) ].dat );
         else
            _pats[i].sim10( _pats[ var(n.fanin[0]) ].dat , _pats[ var(n.fanin[1]) ].dat );
      }else
      {
         if( sign( n.fanin[1] ) )
            _pats[i].sim01( _pats[ var(n.fanin[0]) ].dat , _pats[ var(n.fanin[1]) ].dat );
         else
            _pats[i].sim00( _pats[ var(n.fanin[0]) ].dat , _pats[ var(n.fanin[1]) ].dat );
      }
   }
}
void Fraig::sat2pat_eqset()
{
   uint64_t pat1 = ((uint64_t)1) << (_npat&0x3F) ;
   uint64_t pat0 = ~pat1;
   int    idx  = _npat >> 6;
   _npat +=1;
   assert( idx < PATSIZE );
   for( int s=0 , e=_group[s++]; s!=e ; e=s+_group[s] , s++)
   {
      while( s != e )
      {
         int n = _group[s++];
         if( n < 0 )continue;
         if( (_solver.modelValue( _lits[n] ) == Minisat::lbool((uint8_t)0)) == _ph[n] )
            _pats[n].dat[idx] &= pat0;
         else 
            _pats[n].dat[idx] |= pat1;
      }
   }
}
void Fraig::sat2pat_input()
{   
   uint64_t pat1 = ((uint64_t)1) << (_npat&0x3F) ;
   uint64_t pat0 = ~pat1;
   int    idx  = _npat >> 6;
   _npat +=1;
   for(unsigned i = 1 ; i != _andFlag; ++ i)
   {
      if( _solver.modelValue( _lits[i] ) == Minisat::lbool((uint8_t)0) )
         _pats[i].dat[idx] |= pat1;
      else
         _pats[i].dat[idx] &= pat0;
   }
}
void Fraig::reset_selection()
{
   _npat=0;
   _selptr=1;
   _end=_group[0];
}
///////////////////////////////////////////////////////////////////////////////
//                          PARTITION                                        //
///////////////////////////////////////////////////////////////////////////////
void Fraig::rm_eq_partition()
{
   int *s=_group , *ns=_ngroup;
   int *e=s+*s; s++;
   for( ; s!=e ; e=s+*s, s++ )
   {
      int * c = ns++; *c=*(s-1);
      for( ; s != e ; ++s )
      {
         if( *s == -1) (*c)-=1;
         else *ns++ = *s;
      }
      if( *c == 2 ) ns = c;
   }
   *ns=1;
   std::swap( _group , _ngroup );
}
int Fraig::partition(bool fold)
{
   int *s= _group , *ns= _ngroup;
   int * e = s+*s; s++;

   for( ; s!=e; e= s+*s , s++)
   {
      if( e-s == 2 )
      {
         sub_partition_dual( _pats , _eqn , s , ns );
         continue;
      }

      if(fold)
         for( int * i = s ; i != e ; ++i )
            folding_pattern( _pats[ *i ].dat , Pattern::end , _ph[*i]);

      if( e-s < 24 )
      {
         sub_partition_linear( _pats , _eqn , s , e , ns ); 
         s=e;
      }
      else if ( e -s < 64 )
         sub_partition_sort( _pats , _eqn , s , e , ns );
      else
         sub_partition_hash( _pats , _eqn , _idx , s , e , ns ); 
   }
   *ns  = 1 ;
   std::swap( _group, _ngroup );
   return ns - _group ;
}
///////////////////////////////////////////////////////////////////////////////
//                      PROVE SCHEME                                         //
///////////////////////////////////////////////////////////////////////////////
bool Fraig::prove_eq( int a , int b )
{
   Minisat::Lit x = _lits[a] , y = _lits[b];
   if( _ph[a] ^ _ph[b] )y = ~y;
   return ! ( _solver.solve( x , ~y ) || _solver.solve( ~x , y ) ) ;
}
int Fraig::prove_eq_limit( int a , int b )
{
   Clause v(2); 
   v[0] =  _lits[a] , v[1] = ~_lits[b];

   if( _ph[a] ^ _ph[b] )v[1] = ~v[1];

   _solver.setConfBudget( 100 );
   Minisat::lbool ret = _solver.solveLimited( v );
   if( ret == (Minisat::lbool((uint8_t)2)) )return 2 ; // 2 undef 
   if( ret == (Minisat::lbool((uint8_t)0)) )return 0 ; // sat return 1 --> false 
   
   _solver.setConfBudget( 100 );
   v[0] = ~v[0] , v[1] = ~v[1];
   ret = _solver.solveLimited( v );
   if( ret == (Minisat::lbool((uint8_t)2)) )return 2 ;
   if( ret == (Minisat::lbool((uint8_t)0)) )return 0 ;

   return 1;
}
void Fraig::rm_eq(){ _group[ _selptr ] = -1;}
void Fraig::skip()
{
   _selptr = _end + 1;
   _end = _end + _group[ _end ];
}
int Fraig::select_sig()
{
   _selptr +=1;
   if( _selptr == _end ){ skip(); _selptr+=1; }
   if( _selptr >= _end ) return -1;
   return _group[ _selptr ];
}
///////////////////////////////////////////////////////////////////////////////
//                      MAIN FRAIG FUNCTION                                  //
///////////////////////////////////////////////////////////////////////////////
void Fraig::cover_clause( )
{
   unsigned posize = _po.size();
   for( int s=0 , e=_group[s++]; s!=e ; e=s+_group[s] , s++)
   {
      while( s != e )
      {
         int n = _group[s++];
			if( _focnt[n] != 0 ){
	         _po.push( n+n );
	         _focnt[n] +=1;
			}
      }
   }
   covering();

   assignLit( );
   for( unsigned i = 0 ; i < nVars() ; ++ i ) 
      _solver.newVar();

   _po.downTo( posize );
}
void Fraig::merge()
{
   for( unsigned i = _andFlag; i < sz ; ++ i )
   {
      if( _eqn[i] != i ) 
      {
         conjunct( i , _eqn[i] );
      }
   }
   _focnt.clear();
   create_focnt();
}
void Fraig::feedback()
{
   rm_eq_partition();
   partition(false);
   reset_selection();
   //report();
}
void Fraig::feedback2()
{
   simulation();
   rm_eq_partition();
   partition(true);
   reset_selection();
   //report();
}
// find the dependency level grouping 
void Fraig::eq_dep_level()
{
   int * lvl = _deplvl;

   for( unsigned i = 0 ; i != _andFlag ;++i ) lvl[i] = 0;
   for( unsigned i = _andFlag ; i != sz ; ++ i)
   {
      unsigned v[2] = {var(data[i].fanin[0]), var(data[i].fanin[1])};
      lvl[ i ] = std::max( lvl[ v[0] ]+ (_eqn[v[0]]!=v[0]) , lvl[v[1]]+(_eqn[v[1]]!=v[1]) );
      if( lvl[i] == (int)_stages.size() ) _stages.push();
      _stages[ lvl[i] ].sz+=1;
   }
   unsigned * tmp = new unsigned [sz];
   for( unsigned i = 0 ; i < _stages.size() ; ++i )
   {
      _stages[i].dat = tmp;
      tmp += _stages[i].sz;
   }
   int idx[_stages.size()];
   memset( idx , 0 , sizeof(int)*_stages.size() );
   for( unsigned i = _andFlag ; i != sz ; ++i )
      _stages[ lvl[i] ].dat[ idx[lvl[i]]++ ] = i;
}
void Fraig::grouping()
{
   Pattern::end = 1;
   
   int olit;
   int cnt = 0;
   int THREAD = (1000000 / sz) +1 ;
   
   pat_init_rand();
   simulation();
   olit=partition( true );
   Pattern::end = 128;

   while(1)
   {
      pat_init_rand();
      simulation();
   
      int nlit = partition(true);
      if( olit - nlit < THREAD ) cnt+=1;
      else cnt = cnt>1?(cnt-1):0;
      if( cnt == 4 ) break;
      olit = nlit ;
   }
   //report();
}
void Fraig::run()
{
   grouping();
   if( _group[0]!= 1)
   {
      Pattern::end = 1 ;
      cover_clause();
      assignCNF( _solver );
      _solver.simplify();
      reset_selection();

      for( int s=0 , e=_group[s++]; s!=e ; e=s+_group[s] , s++)
         while( s != e )
         {
            int n = _group[s++];
            _pats[n].dat[0] = 0;
         }
   }
   while( _group[0]!=1 )
   {
      int s = select_sig();
      if( s == -1 )
      {
         if( _npat == 0 ) break;
         feedback();
         continue;
      }
      switch( prove_eq_limit( s , _eqn[s] ) ) 
      {
         case 0 : _eqn[s] = s ; sat2pat_eqset();  skip(); break;
         case 1 : rm_eq(); break;
         case 2 : rm_eq(); _eqn[s] = s ; break;
      }
      if( _npat == 3 ) feedback();
   }
   merge();
}
void Fraig::report()
{
   std::tr1::unordered_set<unsigned> set;

   unsigned group=0 , size=0 , cst=0;
   for( unsigned i = 0 ; i < sz ; ++ i ) 
      if( _eqn[i] != i )
      {
         if( set.find( _eqn[i] ) == set.end() )
         {
            group +=1;
            set.insert( _eqn[i] );
         }
         if( _eqn[i] == 0 ) cst+=1;
         size +=1 ; 
      }
   size += group;
   cout << "cst =\t"<<cst<<"\tcls =\t"<<group<<"\tlit =\t"<<size-group<<endl;
}
#if 0
void Fraig::run2()
{
   grouping();
   if( _group[0] != 1 )
   {
      eq_dep_level();
      cover_clause();
      assignCNF0( _solver );
      reset_selection();
   }
   int lvl=0;
   while( _group[0] != 1 )
   {
      if( lvl != _stages.size() )
      {
         int lim = sz >> 3 ;
         while( lim > 0 && lvl != _stages.size() )
         {
            assignCNF( _solver , _stages[lvl].dat , _stages[lvl].sz );
            lim -= _stages[lvl].sz;
            lvl+=1;
         }
      }
      while(1)
      {
         int s = select_sig();
         if( s == -1 )break;
         if( _deplvl[_eqn[s]] >= lvl ){ skip(); continue;}
         if( _deplvl[s] >= lvl )continue;
         switch( prove_eq_limit( s , _eqn[s] ) ) 
         {
            case 0 : _eqn[s] = s ; sat2pat_input();  skip(); break;
            case 1 : rm_eq(); break;
            case 2 : rm_eq(); _eqn[s] = s ; break;
         }
         if( _npat == 64 ) feedback2();
      }
      if( _npat != 0 )
         feedback2();
      else
      {
         rm_eq_partition();
         reset_selection();
      }
   }
   merge();
}
#endif

